%A brief discussion on when locations with open/running sessions can be updated.
%We could exploit the "preserving" class of updates defined in the LMCS paper.


This section discusses two possible extensions for our framework.
The first one concerns the runtime adaptation 
of processes with active (running) sessions, while the second one concerns the inclusion of recursion and subtyping constructs.
In both cases,  concrete details on the technical machinery required are given, and   the challenges involved are highlighted.

\subsection{Runtime Adaptation of Processes with Active Sessions}
Up to here, our notion of runtime adaptation concerns located processes with no active sessions. 
As already motivated, our intention is to rule careless update actions which may affect the session protocols implemented on such locations.
Here we discuss generalizations of our framework so as to admit the runtime adaptation of located processes containing active sessions. As before, the goal will be to ensure that session communications are %never disrupted by update actions.
both safe and consistent.

To illustrate this point, consider  process $\mathsf{Sys}'$, discussed in the Introduction:
\begin{eqnarray*}
\mathsf{Sys}' \!\!\!& = & \!\!\!\! (\nu \kappa)\big(\scomponent{l_{1}}{\outC{\kappa^{+}}{\mathrm{u_1},\mathrm{p_1}}.\select{\kappa^{+}}{n_1.P_1}.\close{\kappa^{+}}} \para \\ 
& & \qquad \quad \bigscomponent{l_2}{\scomponent{r}{\inC{\kappa^{-}}{u,p}.\branch{\kappa^{-}}{n_1{:}Q_1.\close{\kappa^{-}} \alte n_2{:}Q_2.\close{\kappa^{-}}}\,} \para R \, }\big)
\end{eqnarray*} 

%Consider a located process $\scomponent{l}{P} $ 
\noindent Focusing on location $r$, suppose that 
%and an associated adaptation routine 
$R = \adapt{r}{Q_{\mathsf{X}}}{\mathsf{X}}$.
%Suppose that $P$ contains already established sessions.
There are at least two ways in which $Q_{\mathsf{X}}$ can implement a consistent update on $r$:
\begin{enumerate}[(a)]
\item $Q_{\mathsf{X}}$ \emph{preserves} the behavior at $r$: Intuitively, this means that  $\mathsf{X}$ occurs linearly (exactly once)
in $Q_{\mathsf{X}}$. This way, $Q_{\mathsf{X}}$ may implement a relocation  (as in, e.g., $Q_{\mathsf{X}} = \scomponent{l'}{\mathsf{X}}$, for some different location $l'$) or it may place the behavior at $r$ in a richer context (as in, e.g.,  $Q_{\mathsf{X}} = \scomponent{r}{\mathsf{X} \para R'}$ in which the behavior at location $r$ is \emph{extended} with process $R'$).

\item $Q_{\mathsf{X}}$ \emph{upgrades} the behavior at $P$: This is the case when, e.g., %Intuitively, this means that 
%entails that $Q_{\mathsf{X}} = \scomponent{l}{P'}$ and variable $\mathsf{X}$ does not occur in $P'$. 
$\mathsf{X} \not\in \mathsf{fpv}(Q_{\mathsf{X}})$.
In order to ensure consistency, besides ensuring a compatible interface, the new behavior $Q_{\mathsf{X}}$ should implement all open sessions at $r$ (namely $\kappa^{-}, \kappa^{+}$ above). Therefore, this possibility implies having precise information on the  protocols implemented at $r$, 
for $Q_{\mathsf{X}}$ must continue with such protocols.
\end{enumerate}

%In the rest of the section, we discuss 
\noindent Next we separately consider each of these two alternatives.
%giving technical details on how they 
% can be incorporated in our framework (assuming syntax and typing rules without runtime annotations).
%with running sessions, there are basically two approaches to ensure session consistency: i) the process $P$ is preserved by the update $\adapt{l}{Q}{X}$, i.e., $\mathsf{X}$ appears in $Q$  or ii) a mechanism is needed to share session channels between the process $P$ and the process $Q$. 


\subsubsection{Typing Preserving Updates}\label{ss:pres}
As mentioned above, the key issue in this class of updates is 
%The goal of such restrictions is 
to ensure \emph{linearity} of the processes variable.
Given $\adapt{l}{Q_{\mathsf{X}}}{\mathsf{X}}$, we need to 
guarantee that $\mathsf{X} \in \mathsf{fpv}(Q_{\mathsf{X}})$ (to avoid  discarding the behavior at $l$)
but also that $\mathsf{X}$ occurs exactly once, for duplicating behaviors would be unsound.
A first, but somewhat drastic, way of ensuring linearity would be by adding syntactic restrictions on the shape of 
update contexts (such as  $Q_{\mathsf{X}}$).
We have formalized this alternative is in~\cite[\S\,2.1.2]{BGPZFMOODS}, where behavioral characterizations of update processes are thoroughly analyzed.

%The first strategy is easy to implement, one possible but drastic solution is to require some syntactic restriction on the form of $Q$.
%Notice that not only we require to preserve the process $P$, thus $\mathsf{X} \in \mathsf{fpv}(Q)$,  but we also expect to have  only one occurrence of $\mathsf{X}$ in $Q$ as it would not be reasonable to duplicate behaviors. 
Alternatively, we could exploit the type system, using the information in $\Theta$ to ensure linearity.
%so that exactly one occurrence of $\mathsf{X}$ occurs in $Q$. 
This would require changing rule~\rulename{t:Nil} so that $\nil$ can only be typed in a higher-order environment that contains no process variables.
Also, one would need to refine rule~\rulename{t:Par} so to ensure that process variables are properly split.
More precisely, we would need the following modified rules:
%in $\Theta$ are partitioned among $\Theta_1$ and $\Theta_2$:
$$
\begin{array}{c}
\inferrule*[left=\rulename{t:LNil}]{vdom(\Theta)=\emptyset}{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
\\ \\
\inferrule*[left=\rulename{t:LLoc} ]
 {
       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } }   \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{}{\INT}{P} }{ \type{\ActS}{\INT' }}}
\\ \\
 \inferrule*[left=\rulename{t:LPar}]
 { \judgebis{\env{\Gamma}{\Theta_1}}{P}{\type{\ActS_1}{ \INT_1}} \qquad \judgebis{\env{\Gamma}{\Theta_2}}{Q}{ \type{\ActS_2}{ \INT_2}} \qquad \Theta = \Theta_1 \circ \Theta_2
%  \begin{array}{c}
%\judgebis{\env{\Gamma}{\Theta_1}}{P}{\type{\ActS_1}{ \INT_1}} \qquad
% \judgebis{\env{\Gamma}{\Theta_2}}{Q}{ \type{\ActS_2}{ \INT_2}} \\ \Theta = \Theta_1 \cup \Theta_2 \quad vdom(\Theta_1) \cap vdom(\Theta_2) = \emptyset
%\end{array}
 }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
 \end{array}
$$
where, in $\rulename{t:LPar}$, the splitting 
$\Theta_1 \circ \Theta_2$ is defined if and only if 
$\Theta_1 \cap \Theta_2 = \emptyset$ and $ vdom(\Theta_1) \cap vdom(\Theta_2) = \emptyset$.
Observe that the interplay of these two rules %\rulename{t:Nil'} and \rulename{t:Par'} 
suffices 
to guarantee linearity of process variables.
%that exactly one occurrence of $\mathsf{X}$ occurs in $Q$. 
Indeed, rule~\rulename{t:LPar} ensures that variable $\mathsf{X}$ can be used in at most one subprocess in parallel, whereas rule~\rulename{t:LNil} assures that it is used at least one. Notice also that we keep rule~\rulename{t:Adapt}
as in Table~\ref{tab:ts}: its right-hand side typing ensures that the context does not introduce new open sessions.

With these changes in the typing system, 
the runtime annotation on the number of active sessions (occurring in located process)
can be removed from the reduction semantics. The modified semantics can be found in~\ref{ap:addmat}~(Table \ref{tab:semanticsnoannot}).
% we guarantee that no other open session is introduced in $Q$. 
 
\subsubsection{Typing Runtime Upgrades}
 We now generalize the mechanism in the  previous section to include the \emph{runtime upgrade} of a process $\scomponent{l}{P}$  with a process $Q$ that in particular provides an alternative implementation for the active protocols in $P$. 
As explained earlier, handling an upgrade entails having precise knowledge on the protocols running in the location. 
More precisely, a main challenge is to find a way of %sharing active session 
describing compatibility between the (non bracketed)
endpoints  in $P$ with those in $Q$. We now detail a  possible solution to these issues, based on %handle such knowledge is to introduce a proper reduction 
%defining a typed reduction semantics, 
instrumenting the reduction semantics in \S\,~\ref{ss:opsem} with typing environments. %information. 
Let us consider \emph{typed reductions} of the form:
$$
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} 
\pired 
\judgebis{\env{\Gamma}{\Theta}}{P'}{\type{\ActS'}{\INT'}} 
$$
thus defining how a well-typed process $P$ (and their associated typing and interface) evolve as a result of an internal computation.
We now discuss some selected rules for this typed semantics, given in Table~\ref{tab:selected}; the complete set of rules can be found in~\ref{ap:addmat} (Tables \ref{tab:1typedsemantics} and \ref{tab:typedsemantics}).  

 \begin{table}[t]
 $$
 \begin{array}{lc}
 \rulename{r:ParU}&
 \infer{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{ \type{\ActS_1 \cup \ActS_2}{\INT_1 \cup \INT_2 }} \pired \judgebis{\env{\Gamma}{\Theta}}{P' \para Q}{ \type{\ActS_1' \cup \ActS_2}{\INT_1' \uplus \INT_2' }}}{ \judgebis{\env{\Gamma}{\Theta}}{P }{ \type{\ActS_1}{\INT_1 }} \pired \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS_1'}{\INT_1' }}}
  \\ \\
  \rulename{r:LocU}&
 \infer{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P'}}{ \type{\ActS'}{\INT'}}}{\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT }} \pired \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS'}{\INT'}} }
 \\ \\
 \rulename{r:UpdU}&
\infer{
\begin{array}{c}
\judgebis{\env{\Gamma}{\Theta}}{C\{\scomponent{l}{P}\} \para  D\{\adapt{l}{Q}{X}\}}{\type{\ActS}{\INT}} \\
 \pired \\ %\qquad  \qquad \qquad  \qquad  \\ \qquad  \qquad 
\judgebis{\env{\Gamma}{\Theta}}{C\{\rho(Q)\sub{P}{\mathsf{X}}\}  \para  D\{\nil\}}{\type{\ActS}{(\INT \setminus \INT_1) \uplus \INT_2}}
\end{array}
}
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{\INT_1}} \qquad \judgebis{\env{\Gamma}{\Theta, \mathsf{X}:\ActS_1,\INT_1}}{Q}{\type{\ActS_2}{\INT_2}} \qquad \ActS_1 = \rho(\ActS_2)}
\\ \\
&  
 \judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P\} \para D\{\nopenr{a}{y}.Q\}}{ \type{\ActS}{\INT, a:\alpha_{\qual}, a:\overline{\alpha}_{\qual} }}  \\
\rulename{r:OpenU} & \pired \\
&    \judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C\{P\sub{\cha^+}{x}\} \para D\{Q\sub{\cha^-}{y}}\}}{ \type{\ActS,[\cha^+:\alpha],[\cha^-:\overline{\alpha}]}{\INT}}
 \end{array}
 $$
 \caption{Typed reduction semantics (selected rules).}\label{tab:selected}  
 \end{table}


Main differences with respect to the semantics of Table~\ref{tab:semantics} are:
(i) runtime annotations on locations are no longer needed, and 
(ii) rule $\rulename{r:UpdU}$ checks session consistency by appealing to appropriate typings (denoted $\ActS_1$ and $\ActS_2$ in the rule).
More precisely, as runtime annotations are not considered, typed reduction rules are simpler than untyped ones.
Notice how rule~\rulename{r:LocU} allows us to infer reductions with a single location; 
in general, given a context $C$ (as in Def.~\ref{d:context}) and a process $P$ which may reduce, 
a corresponding typed reduction for process $C\{P\}$  can be inferred by combining rules~\rulename{r:LocU} and \rulename{r:ParU}.
%a filled context can be reduced by the combination of rules  and
Rule \rulename{r:UpdU} 
concerns the update of a located process $P$ with a context $Q$. A typed update reduction will depend on their associated typings, denoted $\ActS_1$ and $\ActS_2$, respectively.
%allows us to replace only processes where the active sessions in $P$ can be matched by the process $Q\sub{P}{\mathsf{X}}$. 
Intuitively, $\ActS_1$ and $\ActS_2$ should be identical, up to a substitution $\rho$ from channel variables $x_1, \ldots, x_m$ in $\ActS_2$
to non bracketed channels $\cha_1^p, \ldots, \cha_m^p$ in $\ActS_1$. 
Substitution $\rho$ works then as an adaptor; to highlight its role, in rule~\rulename{r:UpdU}  we write $\rho(\ActS)$ and $\rho(P)$ to denote the application of $\rho$ to typing $\ActS$ and process $P$; the formal definition of these notations is as expected.
This is how endpoint compatibility between $P$ and $Q$ is enforced. Provided a suitable $\rho$ exists, the 
%To this end, the rule checks whether there exists a suitable assignment $\rho$ such that  type $\ActS_P$ (of active sessions in $P$) matches the type of active sessions in $Q\sub{P}{\mathsf{X}}$: i.e., $\ActS_P = \ActS_Q[\rho]$. If this is the case, the 
upgrade can take place and $\scomponent{l}{P}$ is substituted with  $\rho(Q)\sub{P}{\mathsf{X}}$.


%We start by introducing an assignment function $\rho$ that matches each channels variable $x$ to a channels name $\kappa$,  $\rho$ is used to substitute channel variables in typings $\Delta$ and in processes:  $\Delta[\rho]$ is inductively defined as follows: 
%$$
%\begin{array}{lcl}
% \emptyset[\rho] & =  &\emptyset\\
% (\Delta, \kappa^p:\alpha)[\rho] & = & \Delta[\rho], \kappa^p:\alpha\\
% (\Delta, [\kappa^p:\alpha])[\rho] & = & \Delta[\rho], [\kappa^p:\alpha]\\
% (\Delta, x:\alpha)[\rho] & = & \Delta[\rho], \kappa':\alpha \text{ with } (x,\kappa') \in \rho  
%\end{array}
%$$
%and given a process $P$, $P[\rho]$ represent the systematic substitution of assignments in $\rho$ to process $P$ (i.e., let $\rho = \{(x_1, \kappa_1)\dots (x_n, \kappa_n)\}$ then $P[\rho]=P\sub{x_1}{\kappa_1}\dots\sub{x_n}{\kappa_n}$).

For the system with the typed reduction semantics, we require the   
%is the adaptation of the reduction semantics in Table \ref{tab:semantics} with the 
typing rules in Tables~\ref{tab:ts} and~\ref{tab:session}, replacing rules \rulename{t:Pvar}, \rulename{t:Adapt} and \rulename{t:Loc} with rules  \rulename{t:PVarU}, \rulename{t:AdaptU} and \rulename{t:LocU} below:
$$
\begin{array}{c}
 \inferrule*[left=\rulename{t:PVarU}]{ }{\Gamma; \Theta,\mathsf{X}:\type{\ActS}{\INT} \vdash \mathsf{X}:\type{\ActS}{\INT}}\\ \\

 \inferrule*[left=\rulename{t:AdaptU} ]
{\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:\type{\emptyset}{\INT}}}{P}{\type{\ActS}{ \INT }}}{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{\mathsf{X}}}{\type{\emptyset}{ \emptyset}}} \\ \\

\inferrule*[left=\rulename{t:LocU} ]
 {
       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } }   \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{l}{}{\INT}{P} }{ \type{\ActS}{\INT' }}}
\end{array}
$$

Intuitively, as made explicit by rule~\rulename{t:PVarU}, process variables must now record both a typing $\ActS$ and an interface $\INT$. This refines the intrinsic meaning of an update operation, as there is an explicit reference to required open sessions. 
Based on this enhancement, rule~\rulename{t:AdaptU} is a variant  of rule~\rulename{t:Adapt} in which the process variable occurs annotated with its typing and interface and where we admit a non empty typing $\ActS$, thus allowing process $P$ to introduce active sessions.
Finally, rule~\rulename{t:LocU} simplifies rule~\rulename{t:Loc} by eliminating runtime annotations.
We are confident that session processes in this modified framework also enjoy our safety and consistency results 
(Theorems~\ref{th:subred},~\ref{t:safety}, and \ref{t:consist}) 
 with little modifications.
 %, for the enhanced typed systems and semantics for both preserving and runtime updates. 
% As a consequence we can ensure that a well typed process does not disrupt active communications along its evolution.
 
 

 
%  
% \subsubsection{Typing Upgrades - Cinzia Version}
% 
% The second strategy is clearly more  flexible, we only require that updates do not disrupt established session. In this case, we would like to be able to replace process $P$ with a possibly new implementation of its behavior in $Q$. One possible solution is to extend our semantics  in Table \ref{tab:semantics} to its typed version. 
% 
% 
% Here we admit the possibility of updating adaptable processes with running sessions. To this aim  we require that sessions are preserved by the update, this is obtained by introducing an assignment relation (CINZIA: function or relation??) $\rho$ that matches channels variables in $\Delta_Q$ to channels in $\Delta_P$.
% More precisely $\rho$ associates to variables $x$ channels $\kappa$, thus $\Delta[\rho]$ is inductively defined as follows: 
% $$
% \begin{array}{lcl}
%  \emptyset[\rho] & =  &\emptyset\\
%  (\Delta, \kappa^p:\alpha)[\rho] & = & \Delta[\rho], \kappa^p:\alpha\\
%  (\Delta, [\kappa^p:\alpha])[\rho] & = & \Delta[\rho], [\kappa^p:\alpha]\\
%  (\Delta, x:\alpha)[\rho] & = & \Delta[\rho], \kappa':\alpha \text{ with } (x,\kappa') \in \rho  
% \end{array}
% $$
% Similarly, given a process $P$, $P[\rho]$ represent the systematic substitution of assignments in $\rho$ to process $P$ (i.e., let $\rho = \{(x_1, \kappa_1)\dots (x_n, \kappa_n)\}$ then $P[\rho]=P\sub{x_1}{\kappa_1}\dots\sub{x_n}{\kappa_n}$). All other rules for the typed semantics can be found in Tables~\ref{t:typedltsi},~\ref{t:typedltsii}, and ~\ref{t:typedltsiii} (Page~\pageref{ap:addmat}).
% 
% where $\act \in \{ \kappa^p(\widetilde{c}),\kappa^p(\kappa'^q), \kappa^p(\closeact),  \adapt{l}{Q}{X},\overline{\adapt{l}{Q}{X}}  \}$ and 
% $\overline{\act}$ is defined as follow (notice $\act = \overline{\overline{\act}}$):
% $$
% \begin{array}{lcl}
%  \overline{\kappa^p(\widetilde{c})} &=& \kappa^{\overline{p}}(\widetilde{c})\\
%  \overline{\kappa^p(\kappa'^q)} &=& \kappa^{\overline{p}}(\kappa'^q)\\
%  \overline{\kappa^p(\closeact)} &=& \kappa^{\overline{p}}(\closeact)\\
%  \overline{\adapt{l}{Q}{X}} & = &  \adapt{l}{Q}{X}. 
% \end{array}
% $$
% 
% 
% 
% Notice that with a typed LTS we do not need anymore annotations on adaptable processes and we can get rid of all context rules, apart from rule \rulename{r:Upd} where we still need a context to express all possible nesting of processes.
% 
% 
% % \caption{Typed LTS. }\label{tab:typedsemantics} 
% % \end{table}
% 
% 
% 
% 
% The new semantics presuppose some changes in the type system as well. In particular we need to replace rules \rulename{t:PVar}, \rulename{t:Loc} and \rulename{t:Adapt} of the type system in Tables \ref{tab:ts} and \ref{tab:session} with the following:
% $$
% \begin{array}{c}
% \infer[\rulename{t:PVar}]{\Gamma; \Theta,\mathsf{X}:\ActS,\INT \vdash \mathsf{X}:\type{\ActS}{\INT}}{}
% \\
% \\
%   \infer[\rulename{t:Loc} ]{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P} }{ \type{\ActS}{\INT' }}}
%  {       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } } \qquad \INT' \intpr \INT  }
%  \\
% \\
%  \infer[\rulename{t:Adapt} ]{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}} 
% {\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\ActS_X, \INT}}}{P}{\type{\ActS}{ \INT' }}}.
% \end{array}
% $$
% 
% Another possible solution, that we leave for future work, would be to exploit an operator of \emph{typecase} similar to the one proposed in \cite{DBLP:conf/forte/KouzapasYH11}. This operator would be responsible for the name passing and would allow to apply different update processes depending on the actual type of $P$. 
% 
% %\subsubsection{Typing Upgrades - Jorge Version (Attempt 1)}
% %We now discuss how to type adaptation routines which provide \emph{upgrades}, in which the current behavior at a given location
% %may be replaced at runtime. Notice that an upgrade is a rather flexible option, which subsumes the updates discussed in \S\,\ref{ss:pres}.
% %As motivated earlier, handling upgrades entails having precise knowledge on the protocols running in the location.
% %We now discuss how a \emph{labeled transition system (LTS)} instrumented with type information may offer an alternative to handle such knowledge.
% %Using such a typed LTS we may formalize, for instance, 
% %the replacement of process $P$ (with active protocols/sessions described by $\ActS$) 
% %with a new implementation $Q$ (which realizes the protocols in $\ActS$, possibly adding new behavior).
% %
% %We first comment on some required modifications in the typing rules. We need to 
% %replace rules \rulename{t:PVar}, \rulename{t:Adapt}, and \rulename{t:Loc}  in Table~\ref{tab:ts} with the rules in Table~\ref{tab:upgrade}.
% %Intuitively, as made explicit by rule~\rulename{t:PVarU}, process variables must record both a typing $\ActS$ and an interface $\INT$. This refines the intrinsic meaning of an update operation, as there is an explicit reference to required open sessions. 
% %Based on this enhancement, rule~\rulename{t:AdaptU} is the expected modification 
% %of rule~\rulename{t:Adapt}. Finally, rule~\rulename{t:LocU} is a simplified variant 
% %of \rulename{t:Loc} without runtime annotations.
% %
% %\begin{table}[t!]
% %$$
% %\begin{array}{c}
% %\inferrule*[left=\rulename{t:PVarU}]{ }{\Gamma; \Theta,\mathsf{X}:\ActS,\INT \vdash \mathsf{X}:\type{\ActS}{\INT}}
% % \\
% %\\
% % \inferrule*[left=\rulename{t:AdaptU} ]
% %{\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\ActS, \INT}}}{P}{\type{\ActS'}{ \INT' }} \qquad \ActS \subseteq \ActS'}{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{\mathsf{X}}}{\type{\emptyset}{ \emptyset}}} 
% %\\
% %\\
% %  \inferrule*[left=\rulename{t:LocU} ]
% % {       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } } \qquad \INT' \intpr \INT  }{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P} }{ \type{\ActS}{\INT' }}}
% %
% %\end{array}
% %$$
% %\caption{Typing rules for Upgrade\label{tab:upgrade}}
% %\end{table}
% %
% %The typed LTS defines transitions of the form
% %$$
% %\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} 
% %\xrightarrow{~{\act}~} 
% %\judgebis{\env{\Gamma}{\Theta}}{P'}{\type{\ActS'}{\INT'}} 
% %$$
% %thus capturing the evolution from $P$ to $P'$ by performing an action represented by label $\act$, also in reference to associated typings and interfaces.
% %We define 
% %$$\act \in \big\{\open{a},~ \kappa^p(\widetilde{c}),~\kappa^p(\kappa'^q),~(\nu \kappa'^q)\kappa^p(\kappa'^q),~ \kappa^p(n_j),~\kappa^p(\closeact),~  \adapt{l}{Q}{\mathsf{X}}\big\}$$ 
% %with a notion of dual action, denoted $\overline{\act}$,  defined as 
% %expected (letting $\act = \overline{\overline{\act}}$).
% %In particular, label $\adapt{l}{Q}{\mathsf{X}}$ denotes the action associated to a located processes which adopts an adaptation routine 
% %from its environment. 
% %
% %Table~\ref{t:typedltssel} presents a selection of the rules of the typed LTS. 
% %Rule~\rulename{l:JAdapt} intuitively says that a located process is ready to be updated 
% %by a certain class of adaptation routines; this class is defined by a compatibility on typings, as we explained next.
% 
% 
% \emph{======This approach does not seem to work well, essentially because the check for a compatible update process is made at the side of the located process, which is a bit weird, because of the early scheme. }
% 
% \begin{table}[t!]
% $$
% \begin{array}{c}
% \inferrule*[left=\rulename{l:Accept}]{\INT = \INT' \uplus a:\alpha_{\qual}}{
% \judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\INT}} \xrightarrow{\open{a}} \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS,x:\alpha}{\INT}}}
% \vspace{3mm} \\ 
% \inferrule*[left=\rulename{l:Out}]{\widetilde{e} \downarrow \widetilde{c} \qquad \ActS = \ActS_1,\cha^{p}:!(\tilde{\capab}).\ST \qquad \ActS' = \ActS_1,\cha^{p}: \ST}
% {{\judgebis{\env{\Gamma}{\Theta}}{\outC{\cha^{\,p}}{\widetilde{e}}.P}{ \type{\ActS}{\INT}}  \xrightarrow{\cha^{\,p}(\widetilde{c})}  \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS'}{\INT}}}}
% \vspace{3mm} \\ 
% \inferrule[ \rulename{l:Loc}]
% {\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS'}{\INT'}} }{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{ \type{\ActS}{\INT }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P'}}{ \type{\ActS'}{\INT'}}}
% \vspace{3mm} \\ 
%  \inferrule[\rulename{l:Update}]{ }{
% \judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{Q}{\mathsf{X}}}{\type{\emptyset}{\emptyset}} \xrightarrow{\adapt{l}{Q}{\mathsf{X}}}  
% \judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
% \vspace{3mm} \\ 
%  \inferrule[\rulename{l:Adapt}] 
% {\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_P}{\INT_P}} \quad \judgebis{\env{\Gamma}{\Theta, \mathsf{X}:\ActS_P,\INT_P}}{Q}{\type{\ActS_Q}{\INT_Q}} \qquad \ActS_P = \ActS_Q[\rho]}{
% \judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{\type{\ActS_P}{\INT_P}} \xrightarrow{\overline{\adapt{l}{Q}{X}}} 
% \judgebis{\env{\Gamma}{\Theta}}{Q\sub{P}{\mathsf{X}}[\rho]\}}{\type{\ActS_Q[\rho]}{ \INT_Q}}
% }
% \vspace{3mm} \\ 
% % \inferrule[\rulename{l:JUpdate}]{ }{
% %\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{Q}{\mathsf{X}:\langle \ActS, \INT \rangle}}{\type{\emptyset}{\emptyset}} \xrightarrow{\adapt{l}{Q}{\mathsf{X}:\langle \ActS,\, \INT \rangle}}  
% %\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
% %\vspace{3mm} \\ 
% % \inferrule[\rulename{l:JAdapt}] 
% %{%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} %\qquad \judgebis{\env{\Gamma}{\Theta, \mathsf{X}:\ActS',\INT}}{Q}{\type{\ActS_1}{\INT_1}} 
% %\qquad \rho = \subst{\cha^{p}_1, \ldots, \cha^{p}_m}{x_1, \ldots, x_m} \quad \ActS = \rho(\ActS')}{
% %\judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{\type{\ActS}{\INT}} \xrightarrow{\overline{\adapt{l}{Q}{\mathsf{X}:\langle \ActS',\, \INT\rangle}}} 
% %\judgebis{\env{\Gamma}{\Theta}}{\rho(Q)\sub{P}{\mathsf{X}}}{\type{\ActS}{\INT}}
% %}
% %\vspace{3mm} \\
%  \inferrule[\rulename{l:Com}]
%  { %\begin{array}{c}
% \judgebis{\env{\Gamma}{\Theta}}{P }{ \type{\ActS_1}{\INT_1 }} \xrightarrow{\restr{\widetilde{\cha}}{\act}} \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS_1'}{\INT_1' }}                                                                                                \\
% \judgebis{\env{\Gamma}{\Theta}}{Q }{ \type{\ActS_2}{\INT_2 }} \xrightarrow{\overline{\act}} \judgebis{\env{\Gamma}{\Theta}}{Q'}{ \type{\ActS_2'}{\INT_2' } \qquad \widetilde{\cha} \cap \mathsf{fc}(Q) = \emptyset }
%   %\end{array}
% }
% {\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{ \type{\ActS_1 \cup \ActS_2}{\INT_1 \uplus \INT_2 }} \xrightarrow{~\tau~} 
% \judgebis{\env{\Gamma}{\Theta}}{\restr{\widetilde{\cha}}{(P' \para Q')}}{ \type{\ActS_1' \cup \ActS_2'}{\INT_1' \uplus \INT_2' }}}
% \end{array}
% $$
% \caption{Typed LTS (Selected Rules, from Cinzia's formulation)\label{t:typedltssel}}
% \end{table}
% 
% 
% \subsubsection{Typing Runtime Upgrades - Jorge Version}
% We now discuss how to type adaptation routines which provide \emph{runtime upgrades}, in which the current behavior at a given location, with possibly active sessions, may be replaced at runtime. 
% In general, runtime upgrades subsume the class of updates discussed in \S\,\ref{ss:pres}.
% As explained earlier, handling upgrades entails having precise knowledge on the protocols running in the location.
% Therefore, a main challenge is finding a way of influencing process behavior based on the current state of a protocol, as abstracted by its associated session endpoints.
% 
% To this end, we now discuss how a \emph{labeled transition system (LTS)} instrumented with type information may offer an alternative to handle such knowledge.
% Using such a typed LTS we may formalize, for instance, 
% the replacement of process $P$ (with active protocols/sessions described by $\ActS$) 
% with a process $Q$ (which provides an alternative implementation for the protocols in $\ActS$).
% 
% We first comment on some required changes in the typing rules. Let us %need to 
% replace rules~\rulename{t:PVar}, \rulename{t:Adapt}, and \rulename{t:Loc}  in Table~\ref{tab:ts} with the following ones:
% $$
% \begin{array}{c}
% \inferrule[\rulename{t:PVarU}]{ }{\Gamma; \Theta,\mathsf{X}:\ActS,\INT \vdash \mathsf{X}:\type{\ActS}{\INT}}
% \vspace{3mm} \\
%  \inferrule[\rulename{t:AdaptU} ]
% {\Theta \vdash l:\INT  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\ActS, \INT}}}{P}{\type{\ActS}{ \INT }}}{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{\mathsf{X}:\langle \ActS, \INT\rangle }}{\type{\emptyset}{ \emptyset}}} 
% \hspace{5mm} 
%   \inferrule[\rulename{t:LocU} ]
%  {       \Theta \vdash l:\INT \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT } } }{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P} }{ \type{\ActS}{\INT}}}
%  \end{array}
% $$
% Intuitively, as made explicit by rule~\rulename{t:PVarU}, process variables must now record both a typing $\ActS$ and an interface $\INT$. This refines the intrinsic meaning of an update operation, as there is an explicit reference to required open sessions. 
% Based on this enhancement, rule~\rulename{t:AdaptU} is a variant  
% of rule~\rulename{t:Adapt} in which the process variable occurs annotated with its typing and interface.
% Finally, rule~\rulename{t:LocU} is a simplifies rule~\rulename{t:Loc} by eliminating runtime annotations.
% 
% We now briefly discuss how to formalize runtime adaptation via a typed LTS. We may define transitions of the form
% $$
% \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} 
% \xrightarrow{~{\act}~} 
% \judgebis{\env{\Gamma}{\Theta}}{P'}{\type{\ActS'}{\INT'}} 
% $$
% thus capturing the evolution from $P$ to $P'$ by performing an action represented by label $\act$, also in reference to associated typings and interfaces.
% The set of actions
% $$\act \in \big\{\boldsymbol{\tau},~\open{a},~ \kappa^p(\widetilde{c}),~\kappa^p(\kappa'^q),%~(\nu \kappa'^q)\kappa^p(\kappa'^q),
% ~ \kappa^p(n_j),~\kappa^p(\closeact),~  \adapt{l}{Q}{\mathsf{X}:\langle \ActS, \INT \rangle}\big\}$$ 
% defines labels for the internal action (not to be confused with the base type $\capab$), session establishment, reception of data, channels, and labels, session closure,
% and update reception, respectively.
% The dual  of action $\act$ is denoted $\overline{\act}$; we let $\act = \overline{\overline{\act}}$.
% Intuitions for the set of labels are
% as expected; %: $\boldsymbol{\tau}$ denotes an internal action, 
% we only remark that label $\adapt{l}{Q}{\mathsf{X}:\langle \ActS, \INT \rangle}$ denotes the action associated to a located processes which ``receives'' an adaptation routine $Q$ from its environment. 
% This intuition can be better understood by referring to the transition rules:
% Table~\ref{t:typedltssam} presents a selection of these rules; we describe their informal meaning next.
% \begin{enumerate}[-]
% \item Rules~\rulename{l:Accept} and \rulename{l:Out} define non persistent session acceptance and sending of data within sessions, respectively.
% It is worth noticing how these rules entail modifications in the typing and/or interface of the resulting process(es). 
% \item Rule~\rulename{l:Loc} formalizes transparency of located processes with respect to transitions.
% \item In a loose analogy with an output action in the LTS for the $\pi$-calculus, tule~\rulename{l:JUpdate} signals the availability of an adaptation routine.
% \item Rule~\rulename{l:JAdapt} %intuitively 
% defines runtime adaptation in the ``early style''.
% It says that a located process is ready to be updated 
% by a \emph{compatible} adaptation routine.
% More precisely, given that  $P$, located at $l$, has active sessions denoted by typing $\ActS$ and interface $\INT$,
% this rule says that an update process at $l$ which expects a behavior with typing $\ActS'$ and interface $\INT$ is a suitable candidate 
% for runtime adaptation. Notice that  compatibility is defined as equality of $\ActS$ and $\ActS'$, up to a substitution $\rho$ which
% renames channel variables in $\ActS'$ so as to match channels in $\ActS$. 
% That is, it could be the case that for some $\cha^p:\ST \in \ActS$, it turns out that  $x:\ST \in \ActS'$; then, 
% $\rho$ will include a substitution $\subst{\cha^p}{x}$.
% In this sense, $\rho$ may seen to realize a (very simple) \emph{service adaptor}.
% 
% \item Rule~\rulename{l:Tau} governs the synchronization of dual actions which do not concern channel extrusion. As such, it realizes runtime adaptation relying on \rulename{l:JAdapt} and \rulename{l:JUpdate}.
% \end{enumerate}
% 
% The transition rules for runtime adaptation here given admit generalizations and simplifications, in particular concerning the r\^{o}le of interfaces. Still, they are an appealing way of integrating process and type information, formalized in a way that results to be quite natural for process calculi framework. Part of their appeal resides in the fact that they enable the definition of type-aware reasoning techniques, such as typed behavioral equivalences. 
% A limitation of a typed semantics is the somewhat heavy notations that are required, and the type annotations in processes. Alternative formulations, with simpler notational conventions and reduced type annotations are desirable; this is an interesting (and challenging) issue for future work.
% 
% 
% 
% 
% 
% 
% 
% \begin{table}[t!]
% $$
% \begin{array}{c}
% \inferrule[\rulename{l:Accept}]{\INT = \INT' \uplus a:\alpha_{\qual}}{
% \judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\ActS}{\INT}} \xrightarrow{\open{a}} \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS,x:\alpha}{\INT}}}
% \vspace{3mm} \\ 
% \inferrule[\rulename{l:Out}]{\widetilde{e} \downarrow \widetilde{c} \qquad \ActS = \ActS_1,\cha^{p}:!(\tilde{\capab}).\ST \qquad \ActS' = \ActS_1,\cha^{p}: \ST}
% {{\judgebis{\env{\Gamma}{\Theta}}{\outC{\cha^{\,p}}{\widetilde{e}}.P}{ \type{\ActS}{\INT}}  \xrightarrow{\cha^{\,p}(\widetilde{c})}  \judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS'}{\INT}}}}
% \vspace{3mm} \\ 
% \inferrule[ \rulename{l:Loc}]
% {\judgebis{\env{\Gamma}{\Theta}}{P}{ \type{\ActS}{\INT }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS'}{\INT'}} }{\judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{ \type{\ActS}{\INT }} \xrightarrow{\act} \judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P'}}{ \type{\ActS'}{\INT'}}}
% \vspace{3mm} \\  
%  \inferrule[\rulename{l:JUpdate}]{ }{
% \judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{Q}{\mathsf{X}:\langle \ActS, \INT \rangle}}{\type{\emptyset}{\emptyset}} \xrightarrow{\overline{\adapt{l}{Q}{\mathsf{X}:\langle \ActS,\, \INT \rangle}}}  
% \judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
% \vspace{3mm} \\ 
%  \inferrule[\rulename{l:JAdapt}] 
% {%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} %\qquad \judgebis{\env{\Gamma}{\Theta, \mathsf{X}:\ActS',\INT}}{Q}{\type{\ActS_1}{\INT_1}} 
% \qquad \rho = \subst{\cha^{p}_1, \ldots, \cha^{p}_m}{x_1, \ldots, x_m} \quad \ActS = \rho(\ActS')}{
% \judgebis{\env{\Gamma}{\Theta}}{\scomponent{l}{P}}{\type{\ActS}{\INT}} \xrightarrow{{\adapt{l}{Q}{\mathsf{X}:\langle \ActS',\, \INT\rangle}}} 
% \judgebis{\env{\Gamma}{\Theta}}{\rho(Q)\sub{P}{\mathsf{X}}}{\type{\ActS}{\INT}}
% }
% \vspace{3mm} \\
%  \inferrule[\rulename{l:Tau}]
%  { %\begin{array}{c}
% \judgebis{\env{\Gamma}{\Theta}}{P }{ \type{\ActS_1}{\INT_1 }} \xrightarrow{{\act}} \judgebis{\env{\Gamma}{\Theta}}{P'}{ \type{\ActS_1'}{\INT_1' }}                                                                                                \\
% \judgebis{\env{\Gamma}{\Theta}}{Q }{ \type{\ActS_2}{\INT_2 }} \xrightarrow{\overline{\act}} \judgebis{\env{\Gamma}{\Theta}}{Q'}{ \type{\ActS_2'}{\INT_2' }}
%   %\end{array}
% }
% {\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{ \type{\ActS_1 \cup \ActS_2}{\INT_1 \uplus \INT_2 }} \xrightarrow{~\boldsymbol{\tau}~} 
% \judgebis{\env{\Gamma}{\Theta}}{{P' \para Q'}}{ \type{\ActS_1' \cup \ActS_2'}{\INT_1' \uplus \INT_2' }}}
% \end{array}
% $$
% \caption{A Typed LTS for Session Processes (Selected Rules) \label{t:typedltssam}}
% \end{table}
